\chapter{Introduction}
\label{ch:Introduction}

\sloppy{} Concurrent programming is becoming more important with the
increasing demand for software that runs on highly parallel multi-core
machines, which are now more widespread. 
Many researchers believe that transitioning to multicore processor is a no back
way, and software engineering should follow this way. Nowadays,
all major processor manufacturers have run out of room with
most of their traditional approaches to boosting CPU performance.
 Instead of driving clock speeds ever higher, 
 they are moving processor architecture multicore
 architecture. Multicore architectures are used even in mobile phones, which
 supports the theory that concurrent programming will reach the mainstream
 programming soon. 
Herb Sutter, a researcher that is highly connected with the industry, says that
Concurrency is the next major revolution in how developers write
software~\citep{Sutter:2005:SCR:1095408.1095421}. 
Unfortunately, concurrency
errors are very easy to introduce and difficult to find and reproduce,
in particular, errors related to the undisciplined use of locks in
programs that follow a shared-memory programming model. Even experienced
programmers makes mistakes when developing concurrent programs and they
agree that concurrent program is error prone and much harder than sequential one.
Besides that, errors in concurrent programs are tough to discover reading code
and, sometime, even more tough to discover executing the code!
To prevent such errors, new languages and development methods have been recently
proposed ~\citep{larus-kozyrakis-cacm2008,Burckhardt:2010:CPR,yi-ppopp2011}
and old approaches regained force \citep{lauterburg-etal-ase09}.
Despite all these advances,\Comment{ we believe that} it is still
important to improve the existing support for finding concurrency
errors in shared-memory programs, which remain the dominant
programming model in practice.
A common kind of concurrency error in shared-memory programs is a
\emph{data-race} (or simply race).  The effect of a race is to modify
the program state incorrectly.  A race occurs when execution contains
two accesses to the same memory location that are not ordered by the
happens-before relation and at least one of the accesses is a
write \citep{lamport1978}.  Similar to other kinds of concurrency
errors, a race typically manifests only in rare thread interleaving
and these interleaving are difficult to reproduce.  Programmers
prevent races by protecting potentially conflicting accesses to shared
data with at least one common lock.  However, undisciplined use of
locks can result in other problems such as inefficiency and deadlocks.
Even though data-race free programs do not imply correctness (e.g.,
due to violations of atomicity\Comment{ and ordering} requirements)
and racy programs do not imply incorrectness (e.g., due to the need
for while flags) \citep{shanluEtAl2006}, awareness of low-level
data-races remains important to build correct concurrent programs.

This work proposes a novel approach to find races that
\emph{complements} model-checking by efficiently reporting precise
\emph{warnings} during state-space exploration (SSE): \tname{}.  It
uses information obtained across different paths explored during SSE
to \emph{predict} likely racy memory accesses.  It builds on
the observation that, during state space exploration, memory accesses are
covered much sooner than the actual race occurs.  We evaluated \tname{} on \numCases{}
different scenarios of race, involving a total of \numSubjects{}
distinct application subjects of various sources and sizes.  Results
indicate that \tname{} reports race warnings very soon compared to the
time the model checker detects the race (for \perGoodCases{} of the
cases it reports a true warning of race in $<$5s) and that the
warnings it reports include very few false alarms\Comment{, and that
  the overhead on overall exploration time is, on average, low.}.  We
also observed that the model checker finds the actual race quickly
when it uses a guided-search that builds on \tname{}'s output (for
74.2\% of the cases it reports the race in $<$20s).

\section{Contribution}

The main contribution of this work is a 
novel approach to find data races during model checking state space exploration.
This approach is called rabbit.
It was inspired in the uncertain time that a developer needs to wait to receive an output during model checking.
So, we think in an new approach that could give some feedback to the developer as soon as possible when him start to model checking his code.
The focus of this work is not substitute model checking,
instead of it we propose a technique that complements model checking and is built on top of it.
Our general goal is to enable developers to take action in response to race
warnings before a potentially long search for actual errors finishes. 
And it is exactly what our results suggests.
We believe that rabbit idea is step in direction to bring model checking usage to nonacademic world.



\section{Dissertation Organization}
This work is organized as follows:

\begin{itemize}
\item Chapter~\ref{ch:Background} 
provides an overview of the theoretical basis necessary for understanding this research, 
we explain important concepts like concurrency, data races and details about software model checking and Java Path finder
\item Chapter~\ref{ch:Approach} presents the
Rabbit Idea and gives detailed information about its implementation.
\item Chapter~\ref{ch:Evaluation} introduce a evaluation of the results in a set of well know subject in
verification community.
\item Chapter~\ref{ch:Conclusion} shows our final considerations, related and future works
\end{itemize}


%% the object field
%% and for each of the two accesses include the threads involved,
%% location of the access, the kind of access (read or write), and the
%% lock sets involved.  This report is similar to the one given by 

%% One potential conflict consists of a pair of accesses to the same
%% memory location realized by different threads with the use of disjoint
%% lock sets.  We leverage the fact that stateful model checkers keep
%% object and thread ids fixed along the course of \stsp{}
%% exploration.  This enables \tname{} to relate memory accesses that
%% occur across different schedules to predict potential races rapidly.

\Comment{ For the experiments we considered, the model checker
  identifies no distinct memory accesses after \Fix{N}\% of the states
  are visited, on average.}
\Comment{ The approach is lightweight so to not significantly
  compromise model checking time and space performance to find
  errors.}

\Comment{
It is important to note that software model checkers perform
systematic testing;\Comment{ they do not prove absence of errors only
  their existence.  Therefore,} as such, one would like to explore as
much of the \stsp{} as possible in order to maximize the chances
of finding one error, but it is possible that it takes a lot of time
to find such error, when it indeed exists.}

%%\sloppy Several race-finding approaches have been proposed in the
%%past~(see Section~\ref{sec:related}). 
 
\comment{
\chapter{Objectives}
\label{ch:Objectives}

This reseach focuses on improving
a very popular technique to find races: software model checking.\comment{  A software model checker
takes as input a test driver and explores the \stsp{} of a program,
reachable from the test driver, in seek of errors like races and
deadlocks{~\citep{godefroid97:model,visser03model,robby03:bogor}}. The
approach is sound (i.e., it reports no false positives), however, the
exploration of large \stsp{}s can be very expensive.  In this context,
time efficiency becomes an important requirement: the errors that a
model checker can find are subject to one manually-written test driver
and the runtime cost associated with the exploration of the \stsp{}
from that test driver often can be very high.} As explained in ~\ref{sec:related} model checker explore a huge number of states.  Now, let us suppose
that by only exploring a small fraction of the \stsp{} the model
checker had the capability to identify that a \emph{likely} racy
scheduling would be observed later in the \stsp{} exploration, i.e.,
the model checker could report warnings in addition to accurate error
messages.  We conjecture that, from the user's perspective, the value
of these warnings depends on (a) the ratio of false alarms in the
reported warnings (more important with smaller ratio) and on (b) the
time difference between reporting the warning and the error (more
important the higher the difference).  Under those circumstances, it
will be on the best interest of the user to take action in face of a
potential long wait: to inspect the warning, to fix the error (if that
is indeed positive), and to decide whether or not to stop the search
and spawn a new one considering that the changes could have impacted
the search landscape{~\citep{jagannathEtAl2011}}.

This research presents \emph{\tname{}} to improve the productivity of
model checker users in the task of finding data-race errors.  Our
general goal is to enable users to take action in response to race
warnings before a potentially long search for actual errors finishes.
For example, in one of our experiments we ran the \CodeIn{jpapa}
subject (see~Table~\ref{table:main}) on a popular model checker in
\tname{} mode\Comment{, using depth-search exploration}.  After 1m31s
of exploration, the model checker reports one warning that we
confirmed to be an actual manifestation of race: each warning report
includes information similar to the one reported by the model
checker~(see Figure~\ref{fig:output}).  For this case, the model
checker, running on its default configuration, aborts execution after
1h with an ``out of memory error'' message.

\tname{} builds on our observation that during \stsp{} exploration the
model checker often covers distinct memory accesses much sooner than
covering the actual race, i.e., sooner than exploring one particular
scheduling that reveals the race.  It looks for \emph{potential} races
\emph{during} \stsp{} exploration that can be inferred from these
accesses.  \tname{} uses a search-global identity for objects (and
threads) that enables it to relate objects created across different
exploration paths that a software model checker takes.  \comment{Even though
\tname{} does not have support to detect causally related memory
accesses (which justifies the possibility of false alarms)\Comment{
  and the possibility of loss of object identities (which could result
  in race misses)}, experimental results with \numSubjects{} subjects
and \numCases{} scenarios of errors indicate that it is precise in
practice.  Note that tracking causality is
expensive{~\citep{flanagan-freund-pldi2009}} and would substantially
increase overall cost of software model checking.}  Conceptually, the
precision of \tname{} originates from the use of dynamic information
produced with the \stsp{} exploration: it relates memory accesses
across distinct scheduling at the object and field level.  \tname{}
does not interfere in the search order and its impact on overall
exploration time is low.  To the best of our knowledge \tname{} is the
first attempt to \emph{complement} software model checking, which can
be very expensive, by making it more \emph{responsive} to users.

This research makes the following contributions.\vspace{1ex}

\contr{1}{Idea.}  We propose \tname{}, a novel and lightweight
approach to improve productivity of model checker users in finding
data-race errors.  Our approach anticipates likely future reports of
actual errors.\Comment{ \tname{} efficiently collects coverage
  information of observed runs.}\vspace{0.5ex}

\Comment{ We proposed a technique to optimize model
  checking for a given goal.  The technique operates in two stages:
  one that profiles execution in search of opportunities to reach the
  goal and the other that performs a guided-search}

%% \contr{2}{Application}\Comment{ We instantiated the idea for the
%%   specific context of finding data races in concurrent programs.  In
%%   this context, the profiling stage looks for suspicious accesses to
%%   shared data.  We observed that the profiler obtains precise
%%   information to guide the search and that this information stabilizes
%%   relatively fast}\Fix{...}.
  
\sloppy \contr{2}{Implementation.} We implemented our approach on top
of the Java PathFinder~(JPF)~\citep{visser03model} model
checker.\vspace{0.5ex}

\contr{3}{Experiments.}  We evaluated our approach with \numSubjects{}
subjects from various sources and sizes.  We considered pre-existing
errors and new errors introduced with volunteers during a study.
Considering the \numCases{} different scenarios we analyzed, \tname{}
reported true warnings in less than 5 seconds for 26 cases (78\%).  In
14 of these, JPF without \tname{} takes more than 10
minutes\footnote{We will use the symbol ``s'' for seconds and ``m''
  for minutes.} to find the race (9 cases) or runs out of memory (4
cases) or miss the race (1 case).  Results indicate that users can
benefit the most of our approach for scenarios that produce large
\stsp{}s, that the overhead in JPF exploration time with \tname{}
enabled is low on average ($\sim$\runtimeOverhead{}), and that the
number of false positives is very low.  We also evaluated \tname{}
with different search strategies.  We realized, for example, that
\tname{} with breadth-first search reports true warnings in 5s for all
4 cases where \tname{} with depth-first search takes longer to report
warnings.  Finally, we evaluated the impact of using the output of
\tname{} to drive \jpf's search.  We implemented a heuristic-search
that focuses on the threads involved in the warnings.  We found that
when the search focuses on the threads reported by \tname{} \jpf{}
very often finds the race quickly.  For example, standard \jpf{} takes
11m49s to find a race in the \CodeIn{cache4j} subject while \jpf{}
with \tname's heuristic search finds the error in 1s.  Results
indicate that it is highly beneficial to spawn short-lived executions
of \jpf{} in \tname{} mode using different search strategies (with the
goal of reporting useful warnings) and to spawn short-lived executions
of \jpf{} in heuristic-search mode using different choices of warnings
as reference, i.e., the threads involved in these warnings (with the
goal of finding races fast).

%% considering only the threads involved in the first true warning (a
%% reference scenario for this experiment), JPF with our heuristic-search
%% finds the race in <5s most of the cases.   W

\Comment{ We compared \tname{} with depth-first (DFS) and
  breadth-first (BFS) explorations.  For that, we used several
  applications from the Software-artifact Infrastructure Repository
  (SIR)~\citep{doESE05} used previously to evaluate other bug-finding
  techniques.  Our results indicate that \tname{} reduces on average
  the number of states explored by \dfsStateReduction{} in DFS and by
  \bfsStateReduction{} in BFS, on average.  It reduces time by
  \dfsTimeReduction{} in DFS and by \bfsTimeReduction{} in BFS, on
  average}
}
% LocalWords:  interleavings multi jpapa BIST JPredictor schedules PathFinder
% LocalWords:  JPF pre DFS BFS indicriminated inneficiency atomicity stateful
